\documentclass[a4paper, 11pt, oneside]{elsarticle}

\usepackage{listings}
\usepackage{graphicx} \pdfcompresslevel=9
\usepackage[usenames,dvipsnames]{color}
%\usepackage{cite}
\usepackage{setspace}
\usepackage{float}
\usepackage{fancyhdr}
\usepackage{amsmath, amsthm, amssymb}
\usepackage{algorithmic}
\usepackage{algorithm}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{url}
\usepackage{appendix}
\usepackage{wrapfig}
\usepackage[hang,small,bf]{caption}
\usepackage{alltt}
\usepackage{hyperref}
\usepackage[margin=3cm]{geometry}
\usepackage{bchart}
\usepackage{framed}
\usepackage{mdframed}
\usepackage{graphicx}
\usepackage{lineno}
%\usepackage{times}

\lstset{
	language=bash,
	basicstyle=\small\ttfamily,
	keywordstyle=\bfseries,
	commentstyle=\small\color{blue},
	numbers=left,
	numberstyle=\tiny,
	frame=tb,
	columns=fullflexible,
	showstringspaces=false
}

%****************************************************
%********************   MACROS   ********************
%****************************************************

\newcommand{\HRule}{\rule{\linewidth}{0.5mm}}
\setlength{\parindent}{0in}


\newcommand{\tip}{{\bf T}}
\newcommand{\alc}{\mathcal{ALC}}
\newcommand{\alct}{\mathcal{ALC}+\tip}
\newcommand{\alctmin}{\mathcal{ALC}+\tip_{\mbox{\em min}}}

\newcommand{\hide}[1]{}

\newcommand {\elle} {\mathcal{L}}
\newcommand {\falso} {\bot}
\newcommand {\vero} {\top}
\newcommand {\vuoto} {\emptyset}
\newcommand {\nott} {\lnot}
\newcommand {\tc} {\mid}
\newcommand {\imp} {\rightarrow}
\newcommand {\incluso} {\subseteq}
\newcommand {\appartiene} {\in}
\newcommand {\emme} {\begin{mathcal}M\end{mathcal}}
\newcommand {\enne} {\begin{mathcal}N\end{mathcal}}
\newcommand {\bbox}{\square}
\newcommand {\diverso} {\neq}
\newcommand{\sqset}{\sqsubseteq}
\newcommand{\subs}{\subseteq}
\newcommand{\mint}{\sqcap}
\newcommand{\mun}{\sqcup}
\newcommand {\ellet} {\mathcal{L}_{\bf T}}
\newcommand {\sx} {\langle}
\newcommand {\dx} {\rangle}


%\newcommand{\qed}{{\hspace*{\fill} \rule{2.2mm}{2.2mm}}}

%****************************************************
%******************  ENVIRONMENTS  ******************
%****************************************************

\hide{
\newenvironment{proof}
{\begin{trivlist} \item[] {\bf Proof:}}%
{\qed \end{trivlist}}

\newenvironment{definition}
{\begin{defi} \rm}{\qed \end{defi}}

\newenvironment {proofof}[2]
{\begin{trivlist} \item[] {\bf Proof of #1~\protect{\ref{#2}}.}}%
{\qed \end{trivlist}}


\newenvironment{example}
{\begin{exa} \rm}{\qed \end{exa}}

\newenvironment{remark}
{\begin{rem} \rm}{\end{rem}}
}

\newtheorem{theorem}{Theorem}
\newdefinition{definition}{Definition}
\newdefinition{example}{Example}
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}
%\newproof{proof}{Proof}

\hide{
\newcounter{posu}
\newtheorem{theorem}[posu]{Theorem}
\newtheorem{lemma}[posu]{Lemma}
\newtheorem{corollary}[posu]{Corollary}
\newtheorem{proposition}[posu]{Proposition}
\newtheorem{definition}[posu]{Definition}
\newtheorem{example}[posu]{Example}
\newtheorem{rem}[posu]{Remark}
\newtheorem{proof}[posu]{Proof}
\newtheorem{fact}[posu]{Fact}
}




\begin{document}

%****************************************************
%********************   TITLE   *********************
%****************************************************
\begin{titlepage}
\begin{center}

\begin{figure}[htp]
\centering
\includegraphics[scale=0.25]{img/logo_unito.png}
\label{}
\end{figure}

\textsc{\LARGE Università degli studi di Torino}\\[2cm]
\textsc{\Large Tesi di Laurea Magistrale}\\[2cm]

\HRule \\[0.4cm]
{ \huge \bfseries Thesis title}\\[0.2cm]
\HRule \\[3cm]

% Authors
\begin{flushleft}
{\Large
Candidato:\\[0.5cm]
Luca Violanti}
\end{flushleft}

\end{center}
\end{titlepage}

%****************************************************
%*****************  ABSTRACT  ***********************
%****************************************************

\begin{abstract}
\end{abstract}

\newpage

%****************************************************
%********************  TOC  *************************
%****************************************************

%\tableofcontents


%****************************************************
%***************  INTRODUCTION  *********************
%****************************************************

\chapter{Introduction}

In this thesis we present the design and implementation of a distributed theorem prover for the non-monotonic description logic $\alctmin$.

Description Logics (DL) are a family of formal knowledge representation languages. They are a decidable fragment of the first-order logic formalism used to provide semantics to representation structures.
DLs are used in artificial intelligence for formal reasoning on the concepts of an application domain. It is of particular importance in providing a logical formalism for ontologies and the Semantic Web. The most notable applications outside information science is in bioinformatics and in the codification of medical knowledge. A DL knowledge base (KB) comprises two components: the TBox, containing the definition of concepts (and possibly roles) and a specification of inclusion relations among them, and the ABox containing instances of concepts and roles. Since the very objective of the TBox is to build a taxonomy of concepts, the need of representing prototypical properties and of reasoning about defeasible inheritance of such properties naturally arise. The traditional approach is to handle defeasible inheritance by integrating some kind of nonmonotonic extension of DLs.

%[TODO] completare introduzione

\section{Why}
\section{What}
\section{Logics}
\section{The problem}
\section{Automated reasoning}
\section{State of the art}


%****************************************************
%*********************  DL  *************************
%****************************************************

\chapter{Description Logics}

Research in the field of knowledge representation and reasoning is usually focused on methods for providing high-level descriptions of the world that can be effectively used to build intelligent applications.
In this context, “intelligent” refers to the ability of a system to find implicit consequences of its explicitly represented knowledge.
Such systems are therefore characterized as knowledge-based systems.
Approaches to knowledge representation developed in the 1970’s are sometimes divided roughly into two categories: logic-based formalisms, which evolved out of the intuition that predicate calculus could be used unambiguously to capture facts about the world; and other, non-logic-based representations.
The latter were often developed by building on more cognitive notions for example network structures.
Even though such approaches were often developed for specific representational chores, the resulting formalisms were usually expected to serve in general use.
In other words, the non-logical systems created from very specific lines of thinking (e.g., early Production Systems) evolved to be treated as general purpose tools, expected to be applicable in different domains and on different types of problems.
In a logic-based approach, the representation language is usually a variant of first-order predicate calculus, and reasoning amounts to verifying logical consequence.
In the non-logical approaches, often based on the use of graphical interfaces, knowledge is represented by means of some ad hoc data structures, and reasoning is accomplished by similarly ad hoc procedures that manipulate the structures.
Among these specialized representations we find semantic networks and frames. Owing to their more human-centered origins, the network-based systems were often considered more appealing and more effective from a practical viewpoint than the logical systems.
Unfortunately they were not fully satisfactory because of their usual lack of precise semantic characterization.
The end result of this was that every system behaved differently from the others, in many cases despite virtually identical-looking components and even identical relationship names.

%****************************************************
%******************  DL + T  ************************
%****************************************************

\chapter{Description Logics for typicality}

\section{The logic $\alct$}\label{alct}


In this section, we recall the original $\alct$, which is an extension of $\alc$ by a typicality operator $\tip$ introduced in \cite{FI09}. Given an alphabet of concept names $\mathcal{C}$, of role names $\mathcal{R}$, and of individual constants $\mathcal{O}$, the language $\elle$ of the logic $\alct$ is defined by distinguishing \emph{concepts} and \emph{extended concepts} as follows:

\begin{itemize}
\item (Concepts)
  \begin{itemize}
     \item $A \in \mathcal{C}$, $\vero$ and $\bot$ are \emph{concepts} of
$\elle$;
    \item if $C, D \in \elle$ and $R \in \mathcal{R}$, then $C
\sqcap D, C \sqcup D, \neg C, \forall R.C, \exists R.C$ are
\emph{concepts} of $\elle$
  \end{itemize}
\item (Extended concepts)
    \begin{itemize}
       \item if $C$ is a
concept of $\elle$, then $C$ and $\tip(C)$ are \emph{extended concepts} of $\elle$
     \item boolean combinations of extended concepts are extended
concepts of $\elle$.
    \end{itemize}
\end{itemize}

\noindent  A knowledge base is a pair (TBox, ABox). TBox
contains subsumptions $C \sqsubseteq D$, where $C \in \elle$ is
an extended concept of the form either $C'$ or $\tip(C')$, and $C', D \in
\elle$ are concepts. ABox contains expressions of the form $C(a)$
and $aRb$ where $C \in \elle$ is an extended concept, $R \in
\mathcal{R}$, and $a, b \in \mathcal{O}$.



In order to provide a semantics to the operator $\tip$, we extend the definition of a model used in ``standard''
%terminological logic $\alc$\footnote{We refer to {\cite[handbook]} for a detailed description of the standard Description Logic $\alc$.}:

\begin{definition}[Semantics of $\tip$ with selection function]\label{Semantics
with f_tip} A model is any structure $$\langle \Delta, I, f_\tip \rangle$$
where:

\begin{itemize}
\item $\Delta$ is the domain, whose elements are denoted with $x, y, z, \dots$;
\item $I$ is the extension function that
maps each extended concept $C$
to $C^I \subseteq \Delta$, and each role $R$ to a $R^I \subseteq
\Delta \times \Delta$. $I$ assigns to each atomic concept $A \in
\mathcal{C}$ a set $A^I \subseteq \Delta$ and it is extended to
arbitrary extended concepts as follows:

\begin{itemize}
  \item $\top^I=\Delta$
  \item $\bot^I=\vuoto$
  \item $(\nott C)^I=\Delta \backslash C^I$
  \item $(C \sqcap D)^I=C^I \cap D^I$
  \item $(C \sqcup D)^I=C^I \cup D^I$
  \item $(\forall R.C)^I=\{x \in \Delta \tc \forall y. (x,y) \in R^I \imp y \in C^I\}$
  \item $(\exists R.C)^I=\{x \in \Delta \tc \exists y.(x,y) \in R^I \ \mbox{and} \ y \in C^I\}$
  \item $(\tip(C))^I = f_\tip(C^I)$
\end{itemize}


\item Given $S \subseteq \Delta$, $f_\tip$ is a function $f_\tip : Pow(\Delta) \rightarrow Pow(\Delta)$
satisfying the
following properties:

\begin{itemize}
\item $(f_\tip-1)$ $f_\tip(S) \subseteq S$;
\item $(f_\tip-2)$ if $S \neq \emptyset$, then also $f_\tip(S)
\neq \emptyset$;
\item $(f_\tip-3)$ if $f_\tip(S) \subseteq R$, then $f_\tip(S) = f_\tip(S \cap R)$;
 \item $(f_\tip-4)$ $f_\tip(\bigcup S_i ) \subseteq \bigcup f_\tip(S_i)$;
\item $(f_\tip-5)$ $\bigcap f_\tip(S_i) \subseteq  f_\tip(\bigcup S_i)$.
\end{itemize}

\end{itemize}

\end{definition}

\noindent Intuitively, given the extension of some concept $C$,
the selection function $f_\tip$ selects  the {\em typical}
instances of $C$. ($f_\tip-1$) requests that typical elements of
$S$ belong to $S$. ($f_\tip-2$) requests that if there are
elements in $S$, then there are also {\em typical} such elements.
The following properties constrain the behavior of $f_\tip$ with
respect to $\cap$ and $\cup$ in such a way that they do not entail
monotonicity. According to ($f_\tip-3$), if the typical elements
of $S$ are in $R$, then they coincide with the typical elements of
$S \cap R$, thus expressing a weak form of monotonicity (namely,
{\em cautious monotonicity}). ($f_\tip-4$) corresponds to one
direction of the equivalence $f_\tip(\bigcup S_i) = \bigcup
f_\tip(S_i)$, so that it does not entail monotonicity. Similar
considerations apply to the equation $f_\tip(\bigcap S_i) =
\bigcap f_\tip(S_i)$, of which only the inclusion $\bigcap
f_\tip(S_i) \incluso f_\tip(\bigcap S_i)$ holds. ($f_\tip-5$) is a
further constraint on the behavior of $f_\tip$ with respect to
arbitrary unions and intersections; it would be derivable if
$f_\tip$ were monotonic.



In \cite{FI09}, we have shown that one can give an equivalent,
alternative semantics for $\tip$ based on a \emph{preference
relation} semantics rather than on a selection function semantics.
The idea is that there is a global, irreflexive and transitive
relation among individuals and that the typical members of a
concept $C$ (i.e., those selected by $f_\tip(C^I)$) are the
minimal elements of $C$ with respect to this relation. Observe
that this notion is \emph{global}, that is to say, it does not
compare individuals with respect to a specific concept. For this
reason,  we cannot express the fact that  $y$ is more typical than
$x$ with respect to concept $C$, whereas $x$ is more typical than
$y$ with respect to another concept $D$. All what we can say is
that either $x$ is incomparable with $y$ or $x$ is more typical
than $y$ or $y$ is more typical than $x$. In this framework, an
element $x \in \Delta$ is a {\em typical instance} of some concept
$C$ if $x \in C^I$ and there is no $C$-element in $\Delta$ {\em
more typical} than $x$. The typicality preference relation is
partial since it is not always possible to establish given two
element which one of the two is more typical. Following KLM, the
preference relation also satisfies a \emph{Smoothness Condition},
which is related to the well known \emph{Limit Assumption} in
Conditional Logics \cite{Nute80} \footnote{More precisely,
the Limit Assumption entails the Smoothness Condition (i.e. that
there are no infinite $<$ descending chains). Both properties come
for free in finite models.}; this condition ensures that, if the
extension $C^I$ of a concept $C$ is not empty, then there is at
least one \emph{minimal} element of $C^I$. This is stated in a
rigorous manner in the following definition:

\begin{definition}\label{Definition of $<$} Given an irreflexive and transitive relation  $<$ over a domain
$\Delta$, called \emph{preference relation}, for all $S \subseteq \Delta$,
 we define

 $$Min_<(S)= \{x \in S \tc \nexists y \in S \ \mbox{s.t.} \ y < x \}$$


\noindent We say that $<$ satisfies the {\em Smoothness Condition}
if for all $S \subseteq \Delta$, for all $x \in S$, either $x \in Min_<(S)$ or
$\exists y \in  Min_<(S)$ such that $y < x$.
\end{definition}


\noindent The following representation theorem is proved in \cite{FI09}:

\begin{theorem}[Theorem 2.1 in \cite{FI09}]\label{rtrt} Given any model $\langle \Delta, I, f_\tip
\rangle$,
  $f_\tip$ satisfies postulates $(f_\tip-1)$ to $(f_\tip-5)$ above iff there exists  an irreflexive and transitive relation $<$ on $\Delta$,
satisfying the Smoothness Condition, such that for all $S \subseteq \Delta$, $f_\tip(S)
= Min_<(S)$.
\end{theorem}


\noindent Having the above Representation Theorem, from now on, we will refer
to the following semantics:

\begin{definition}[Semantics of $\alct$]\label{Semantics of T} A model $\emme$ of $\alct$ is any
structure $$\langle \Delta, I, < \rangle$$ where:

\begin{itemize}

\item $\Delta$ is the domain;

\item $<$ is an irreflexive and transitive
relation over $\Delta$ satisfying the Smoothness
Condition (Definition \ref{Definition of $<$})

\item $I$ is the extension function that
maps each  extended concept $C$ to $C^I \subseteq \Delta$, and
each role $R$ to a $R^I \subseteq \Delta \times \Delta$. $I$
assigns to each atomic concept $A \in \mathcal{C}$ a set $A^I
\subseteq \Delta$. Furthermore, $I$ is extended as in Definition
\ref{Semantics with f_tip} with the exception of $(\tip(C))^I$,
which is defined as
$$(\tip(C))^I = Min_<(C^I).$$
\end{itemize}

\end{definition}

 \noindent Let us now introduce the notion of
satisfiability of an $\alct$ knowledge base. In order to define the semantics of the assertions of the ABox, we  extend
the function $I$ to individual constants;  we assign to each individual constant $a \in \mathcal{O}$ a
\emph{distinct} domain element $a^I \in \Delta$, that is to say we enforce the \emph{unique name assumption}.
As usual, the adoption of the  unique name assumption greatly simplifies reasoning about
prototypical properties of individuals denoted by different individual constants.
Considering the example of department staff having lunches, if (in addition to the TBox) the ABox only contains the following facts about Greg and Sara:

\begin{quote}
$\mathit{DepartmentMember}(\mathit{greg})$ \\
$\mathit{DepartmentMember}(\mathit{sara}), \mathit{TemporaryWorker}(\mathit{sara})$
\end{quote}

\noindent we would like to infer that Greg takes his lunches at the restaurant, whereas Sara does not; but without the unique name hypothesis,
we cannot get this conclusion since Greg and Sara might be the same individual.
To perform useful reasoning we would need to  extend the language with equality and make a case
analysis according to possible identities of individuals. While this is technically possible,
we prefer to keep the things simple here by adopting the unique name assumption.



\begin{definition}[Model satisfying a Knowledge Base]\label{Def-ModelSatTBox-ABox}
Consider a model $\emme$, as defined in Definition \ref{Semantics
of T}. We extend $I$ so that it assigns to each individual
constant $a$ of $\mathcal{O}$ an element $a^I \in \Delta$,  and $I$ satisfies the unique name assumption. Given a KB (TBox,ABox), we say that:

\begin{itemize}
\item $\emme$  satisfies TBox iff  for all  inclusions $C \sqsubseteq D$  in TBox, $C^I \subseteq D^I$.
\item $\emme$ satisfies ABox  iff:
(i) for all $C(a)$  in ABox, we have that $a^I \in C^I$,
(ii) for all $aRb$ in ABox, we have that $(a^I,b^I) \in R^I$.
\end{itemize}

\noindent $\emme$ satisfies a knowledge base if it satisfies both
its TBox and its ABox.  Last, a query $F$  is  entailed by KB in
$\alct$ if it holds in all models satisfying \emph{KB}. In this
case we write \emph{KB} $\models_{\alct} F$.
\end{definition}






\noindent Notice that the meaning of $\tip$ can be split into two parts: for any
$x$ of the domain $\Delta$,  $x \in (\tip(C))^I$ just in case
(i) $x \in C^I$, and (ii) there is no $y \in C^I$ such that $y < x$. As already mentioned in the Introduction,
in order to isolate the second part of the meaning of $\tip$ (for the
purpose of the calculus that we will present in Section \ref{calcolo}), we introduce
a new modality $\bbox$. The basic idea is simply to interpret the preference
relation $<$ as an accessibility relation. By the Smoothness
Condition, it turns out that $\bbox$ has the
properties as in G\"odel-L\"ob modal logic of provability G. The
Smoothness Condition ensures that typical elements of $C^I$ exist
whenever $C^I \diverso \vuoto$, by avoiding infinitely
descending chains of elements. This condition therefore
corresponds to the finite-chain condition on the accessibility
relation (as in G).
The interpretation of $\bbox$ in $\emme$ is as follows:

\begin{definition}\label{def-box}
Given a model $\emme$ as in Definition \ref{Semantics of T}, we extend the definition of $I$ with the following clause:
\begin{center}
      $ (\bbox C)^I = \{x \in \Delta \tc $  for every $y \appartiene \Delta$, if
    $y < x$ then $y \in C^I \}$
\end{center}
\end{definition}


\noindent It is easy to observe that $x$ is a typical instance  of $C$ if and only if it is an instance of $C$ and $\bbox \nott C$, that is to say:

\begin{proposition}\label{Relation between T an box}
Given a model $\emme$ as in Definition \ref{Semantics of T}, given a concept $C$ and an element $x \in \Delta$, we have that
$$x \in (\tip(C))^I \ \mbox{iff} \  x \in (C \sqcap \bbox \neg C)^I$$
\end{proposition}

\noindent
Since we only use $\bbox$ to capture the meaning of $\tip$, in the
following we will always use the modality $\bbox$ followed by a negated concept,
as in $\bbox \neg C$.

The Smoothness condition, together with the transitivity of $<$, ensures the following Lemma:

\begin{lemma}\label{ssc}
Given an $\alct$ model as in Definition \ref{Semantics of T}, an extended concept $C$, and an element $x \in \Delta$, if there exists $y < x$ such that $y \in C^I$, then either $y \in Min_<(C^I)$ or there is $z<x$ such that $z \in Min_<(C^I)$.
\end{lemma}
\begin{proof}
Since $y \in C^I$, by the Smoothness Condition we have that either (i) $y \in Min_<(C^I)$ or (ii) there is $z<y$ such that $z \in Min_<(C^I)$. In case (i) we are done. In case (ii), since $<$ is transitive, we have also that $z< x$ and we are done.
\end{proof}


Last, we state a theorem which will be used in the following:

\begin{theorem}[Finite model property of $\alct$]\label{fmpALCT}
The logic $\alct$ has the finite model property.
\end{theorem}

\begin{proof}
The theorem is a consequence of Theorems 3.1 and 3.2 in \cite{FI09},
which prove the soundness, the completeness and the termination of a tableau calculus for $\alct$. Indeed, if
a KB is satisfiable in an $\alct$ model, then there is a tableau with a finite open branch. With a construction similar to the one
used in the proof of Theorem 3.1, from this branch we can build a finite model satisfying KB.
\end{proof}



\section{The logic $\alctmin$}\label{alctmin}

As mentioned in the Introduction, the logic $\alct$ presented in
\cite{FI09} allows  to reason about typicality. As a difference
with respect to standard $\alc$, in $\alct$ we can consistently
express, for instance, the fact that three different concepts,
like {\em Department member}, {\em Temporary Department Member}
and {\em Temporary Department member having restaurant tickets},
have a different status with respect to {\em Have lunch at a
restaurant}. This can be consistently expressed by including in a
knowledge base the three formulas:

\begin{quote}
$\tip (\mathit{DepartmentMember}) \sqset \mathit{LunchAtRestaurant}$\\
$\tip (\mathit{DepartmentMember} \mint \mathit{TemporaryResearcher})  \sqset \nott \mathit{LunchAtRestaurant}$\\
$\tip (\mathit{DepartmentMember} \mint \mathit{TemporaryResearcher} \mint \exists \mathit{Owns}.\mathit{RestaurantTicket})  \sqset \mathit{LunchAtRestaurant}$
\end{quote}

\noindent Assume that $\mathit{greg}$ is an instance of the concept
$\mathit{DepartmentMember} \sqcap \mathit{TemporaryResearcher} \sqcap \exists \mathit{Owns}.\mathit{RestaurantTicket}$. What can we conclude about
$\mathit{\mathit{greg}}$? We have already mentioned that if the ABox explicitly points out that $\mathit{greg}$ is a {\em typical} instance of the  concept, and it contains the assertion that:

$$(*)  \ \tip(\mathit{DepartmentMember} \sqcap \mathit{TemporaryResearcher} \sqcap \exists \mathit{Owns}.\mathit{RestaurantTicket})(\mathit{greg}),$$


\noindent then, in $\alct$, we can conclude
that

$$\mathit{LunchAtRestaurant(\mathit{greg})}.$$

\noindent However, if (*) is replaced by the weaker
$$(**)  \ (\mathit{DepartmentMember} \sqcap \mathit{TemporaryResearcher} \sqcap \exists \mathit{Owns}.\mathit{RestaurantTicket})(\mathit{greg}),$$ in which
there is no information about the typicality of $\mathit{greg}$,
in $\alct$ we can no longer draw this conclusion, and indeed we
cannot make any inference about whether $\mathit{greg}$ spends its
lunch time at a restaurant or not. The limitation here lies in the
fact that $\alct$ is {\em monotonic}, whereas we would like to
make a non-monotonic inference. Indeed, we would like to
non-monotonically assume, in the absence of information to the
contrary, that $\mathit{greg}$ is a typical instance of the
concept. In general, we would like to infer that individuals are
typical instances of the concepts they belong to, if this is
consistent with the KB.

As a difference with respect to $\alct$, $\alctmin$ is {\em non-monotonic}, and it allows to make this kind of inference. Indeed, in $\alctmin$ if (**) is all the information about $\mathit{greg}$ present in the ABox, we can derive that $\mathit{greg}$ is a typical instance of the concept, and from the inclusions above we conclude that $\mathit{LunchAtRestaurant(\mathit{greg})}.$
 We have already mentioned that we obtain this non-monotonic behaviour by restricting our attention to the  minimal $\alct$ models. As a difference with respect to $\alct$,
 in order to determine what is entailed by  a given knowledge base KB, we do not consider {\em all} models of KB but only the {\em minimal} ones. These are the models that minimize the number of atypical instances of  concepts.

Given a KB, we consider a finite set $\ellet$ of concepts
occurring in the KB: these are the concepts for which we want to
minimize the atypical instances.
%Our purpose is that of maximizing the typicality of all
%instances of the concepts in $\ellet$,
The minimization of the set of atypical instances will apply to
individuals explicitly occurring in the ABox as well as to
implicit individuals. We assume that the set $\ellet$ contains at
least all concepts $C$ such that $\tip(C)$ occurs in the KB.
Notice that in case $\ellet$ contains more concepts than
those occurring in the scope of $\tip$ in KB, the atypical
instances of these concepts will be minimized but no extra
properties will be inferred for the typical instances of the
concepts, since the KB does not say anything about these
instances.

% individuals implicitly defined in the KB.

%The preference relation among models, informally, allows a model
%$\emme$ to be preferred to a model $\enne$, when $\emme$ contains
%more typical instances of the concepts in {\cal C} than $\enne$.

We have seen that $(\tip(C))^I =(C \sqcap \bbox \neg C)^I$: $x$ is
a typical instance  of a concept $C$ ($x \in (\tip(C))^I$) when it
is an instance of $C$  and there is no other instance of $C$
preferred to $x$, i.e. $x \in (C \sqcap \bbox \neg C)^I$. By
contraposition an instance of $C$ is atypical if $x \in (\neg
\bbox \neg C)^I$ therefore in order to minimize the atypical
instances of $C$, we minimize the instances of $\neg \bbox \neg
C$. Notice that this is different from maximizing the instances of
$\tip(C)$. We have adopted this solution since it allows to
maximize the set of typical instances of $C$ without affecting the
extension $C^I$ of $C$ (whereas maximizing the extension of
$\tip(C)$  would imply maximizing also the extension of $C$).

%for those $C \in \ellet$.

We define the set $\emme^{\bbox^-}_{\ellet}$ of negated boxed
formulas holding in a model, relative to the concepts in
$\ellet$:


\begin{definition}
Given a model $\emme=\sx \Delta, I, <\dx$ and a set of concepts $\ellet$, we define
$$\emme^{\bbox^-}_{\ellet}=\{(x, \nott \bbox \nott C) \tc x \in (\nott \bbox \nott C)^I, \ \mbox{with} \ x \in \Delta, C \in
\ellet \}$$
\end{definition}


\noindent Let KB be a knowledge base and let ${\ellet}$ be a set of concepts
occurring in KB.

\begin{definition}[Preferred and minimal models]\label{def preferred and minimal models}
Given a model $\emme=\sx \Delta_{\emme}, I_{\emme}, <_{\emme} \dx$ of KB
and  a model $\enne=\sx \Delta_{\enne}, I_{\enne}, <_{\enne} \dx$ of KB,
we say that $\emme$ is preferred to $\enne$ with respect to
${\ellet}$, and we write $\emme <_{\ellet} \enne$, if the
following conditions hold:

\begin{itemize}
\item $\Delta_{\emme}=\Delta_{\enne}$
\item $a^{I_{\emme}}=a^{I_{\enne}}$ for all individual constants $a \in \begin{mathcal}O\end{mathcal}$
\item $\emme^{\bbox^-}_{\ellet} \subset \enne^{\bbox^-}_{\ellet}$.
\end{itemize}

 \noindent A model $\emme$ is a \emph{minimal model} for KB (with respect to
${\ellet}$) if it is a model of KB and there is no a model
$\emme'$ of KB such that $\emme' <_{\ellet} \emme$.
\end{definition}

\noindent Given the notion of preferred and minimal models above, we introduce a notion of \emph{minimal entailment}, that is to say we restrict our consideration to minimal models only. First of all,
we introduce the notion of \emph{query}, which can be minimally entailed from a given KB.
A query $F$ is  a formula of the form $C(a)$ where $C$ is an extended concept and $a \in \mathcal{O}$.
We assume that, for all $\tip(C')$ occurring in $F$, $C' \in \ellet$.
Given a KB and a model $\emme=\sx \Delta, I, < \dx$ satisfying it, we say that a query $C(a)$ holds in $\emme$ if $a^I \in C^I$.

Let us now define minimal entailment of a query in $\alctmin$. In
Section \ref{sec:altri problemi di ragionamento} we will reduce
the other  standard reasoning tasks to minimal entailment.

\begin{definition}[Minimal Entailment in $\alctmin$]\label{LogicalConsequenceALCTMIN}
A query $F$  is minimally entailed from a
knowledge base \emph{KB} with respect to ${\ellet}$ if it holds in all
models of \emph{KB} that are minimal with respect to ${\ellet}$. We write \emph{KB}
$\models_{min}^{\ellet} F$.
\end{definition}


\noindent The non-monotonic character of $\alctmin$ also allows to deal with the following examples.

\vspace{0.5cm}


\noindent {\em Example 1}.
Consider the following KB:
$$\mbox{KB} \ = \{ \tip(\mathit{Athlet}) \sqset
\mathit{Confident}, \mathit{Athlet}(\mathit{john}),
\mathit{Finnish}(\mathit{john})\}$$ and ${\ellet}=
\{\mathit{Athlet}, \mathit{Finnish}\}$. We have $$\mbox{KB} \
\models_{min}^{\ellet} \mathit{Confident}(\mathit{john})$$
%If we restrict our attention to minimal models, we derive $T(i)$.
Indeed, there is no minimal model of KB that contains a non typical instance of some concept (indeed in all minimal models of KB the relation $<$ is empty).
Hence $\mathit{john}$ is an instance of $\tip(\mathit{Athlet})$
(it can be easily verified that any model in which $\mathit{john}$
is not an instance of $\tip(\mathit{Athlet})$ is not minimal).  By
KB, in all these models, $\mathit{john}$ is an instance of
$\mathit{Confident}$. Observe that $\mathit{Confident}(\mathit{john})$ is obtained, in spite of the
presence of the irrelevant assertion
$\mathit{Finnish}(\mathit{john})$.


\vspace{0.35cm}

\noindent {\em Example 2}. Consider now the knowledge base KB' obtained by adding to KB the
formula $\tip(\mathit{Athlet} \mint \mathit{Finnish}) \sqsubseteq \neg \mathit{Confident}$, that is to say:
$$\mbox{KB'}  = \{ \tip(\mathit{Athlet}) \sqset \mathit{Confident}, \tip(\mathit{Athlet} \ \mint \ \mathit{Finnish}) \sqsubseteq \neg \mathit{Confident},
\mathit{Athlet}(\mathit{john}), \mathit{Finnish}(\mathit{john})\}$$
and to ${\ellet}$ concept
$\mathit{Athlet} \mint \mathit{Finnish}$. From KB', $\mathit{Confident}(\mathit{john})$ is no longer derivable.
Instead, we have that $$\mbox{KB}' \models_{min}^{\ellet} \neg \mathit{Confident}(\mathit{john}).$$ Indeed, by reasoning as above it can be shown that in all the minimal models of KB', $\mathit{john}$ is an instance of $\tip(\mathit{Athlet} \mint \mathit{Finnish})$, and it is
no longer an instance of $\tip(\mathit{Athlet})$. This example shows that, in case of
conflict (here, $\mathit{john}$ cannot be both a typical instance of $\mathit{Athlet}$ and of
$\mathit{Athlet} \mint \mathit{Finnish}$), typicality in the more specific concept is
preferred.

\vspace{0.35cm}

\noindent In general, a knowledge base KB may have no minimal model or more
than one minimal model, with respect to a given $\ellet$. The following properties hold.

\begin{proposition}\label{proprModMinimali1}
If \emph{KB} has a model, then \emph{KB} has a minimal model with respect to
any $\ellet$.
\end{proposition}

The above fact  is  a consequence of the \emph{finite model property} of the logic $\alct$ (Theorem \ref{fmpALCT}).


\begin{proposition}\label{proprModMinimali2} Given a knowledge base \emph{KB} and a query $F$, let us replace
all occurrences of  $\tip(C)$ in \emph{KB} and in $F$ with $C$. We
call  \emph{KB'} the resulting knowledge base and $F'$ the
resulting query. If \emph{KB} $\models_{min}^{\ellet} F$ then
\emph{KB'} $\models_{\alct} F'$.
\end{proposition}
\begin{proof} We show the contrapositive that if
KB' $\not\models_{\alct} F'$ then KB
$\not\models_{min}^{\ellet} F$. Let $\emme$ be an $\alct$ model
satisfying KB' and not satisfying $F'$. Since neither
KB' nor $F'$ contain any occurrence of $\tip$, the relation $<$ does not
play any role in $\emme$ and we can assume that  $<$ is empty.
Notice that in $\emme$, for all $C$, we have that $\tip(C)^I = C^I$. Therefore it
can be shown by induction on the complexity of formulas in
KB and in $F$ that $\emme$ is also a model of KB that
does not satisfy $F$.

Furthermore,  by Definition \ref{def-box}, for all $C$: $(\neg
\bbox \neg C)^I = \emptyset$, hence $\emme$ is a minimal model of
KB. We therefore conclude that KB
$\not\models_{min}^{\ellet} F$, and the proposition follows by
contraposition.
\end{proof}




 The above proposition shows that the inferences
allowed by $\alctmin$ have as  upper approximation the
consequences that can be drawn classically from the knowledge base
\emph{KB'} obtained by  transforming $\tip(C) \sqset C'$ into the
trivial  $C \sqset C'$, what corresponds to  assume that all
individuals are typical. Obviously the \emph{KB'} may be
inconsistent or degenerated (all concepts are empty), whereas the
original \emph{KB} is not. For this reason the inverse of
the proposition obviously does not hold.




\chapter{Background}
\section{Logics}
\section{Calculus}
\section{Implementation}

\chapter{Architecture}

\chapter{Conclusion}






%\vskip 0.2in
\bibliographystyle{elsarticle-harv}
\bibliography{biblioMarzo2010}




\end{document}
@
